\begin{tabbing}
$\forall$${\it es}$:ES, ${\it ff}$:FIFO, ${\it f2f+}$:F2F+{-}decls.
\\[0ex]plus{-}ify\{i:l\}(${\it es}$;${\it ff}$;is\_req  ;is\_ack ;awaiting ;owes\_ack )
\\[0ex]$\Rightarrow$ \=($\forall$${\it sndr}$, ${\it rcvr}$:${\it ff}$.C.\+
\\[0ex]($\exists$$m$:E. ([$m$: ${\it sndr}$ $--$is\_req  $\rightarrow$ ${\it rcvr}$] $\vee$ [$m$: ${\it rcvr}$ $--$is\_ack $\rightarrow$ ${\it sndr}$]))
\\[0ex]$\Rightarrow$ ($\exists$\=$m$:E\+
\\[0ex](([$m$: ${\it sndr}$ $--$is\_req  $\rightarrow$ ${\it rcvr}$] $\vee$ [$m$: ${\it rcvr}$ $--$is\_ack $\rightarrow$ ${\it sndr}$])
\\[0ex]\& (\=$\forall$$y$:E.\+
\\[0ex]([$y$: ${\it sndr}$ $--$is\_req  $\rightarrow$ ${\it rcvr}$] $\vee$ [$y$: ${\it rcvr}$ $--$is\_ack $\rightarrow$ ${\it sndr}$])
\\[0ex]$\Rightarrow$ (($y$ = $m$) $\vee$ ($\exists$$z$:E. f2f+{-}pred($z$,$y$)))))))
\-\-\-
\end{tabbing}